es:ES, i, x, y:Id, Tx, Ty:Type, P:(TxTy), Lx, Ly:(Knd List).
@i only Lx affect x:Tx
 @i only Ly affect y:Ty
 @i(x:Tx)
 @i(y:Ty)
 e@i. (kind(e)  Lx @ Ly)  P(x when e,y when e)  P((x after e),(y after e))
 @i stable state.P(state.x,state.y)   

latex

Definitions

(x  l), kind(e), as @ bs, Knd, x. t(x), @i only L affect x:T, A c B, {x:A| B(x)} , s.x, @i stable state.P(state)  , (discrete state when e), (discrete state after e), if b then t else f fi , Unit, discrete(i;x), , b, b, loc(e), t.1, let x,y = A in B(x;y), Atom$n, s ~ t, Id, SQType(T), {T}, @i(x:T), vartype(i;x), e@i. P(e), Dec(P), , Type, f(a), s = t, <a, b>, (x after e), x when e, Void, A, False, P  Q, P & Q, x:A  B(x), P  Q, x(s1,s2), x:AB(x), P  Q, P  Q, left + right, E, x:A. B(x), type List, t  T, ES, l[i], i z j, i <z j, hd(l)

Lemmas

event system wf, Knd wf, es-E wf, es-kind wf, l member wf, member append, append wf, decidable equal Kind, decidable l member, es-vartype wf, Id sq, Id wf, es-when wf, assert wf, not wf, bnot wf, bool wf, es-isconst wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-loc wf, es-after wf, es-frame wf, es-dtype wf, alle-at wf